Asking for opinions here

• Should we move all the telescopes outside of contrib and into a library or into base? If so which one?

My opinion is that it should be moved outside contrib because shrinking the library with no single idea is a good thing. I think it should go to a separate library rather than to base, because I don't feel this thing needs to be in base. Maybe I feel so because I haven't used this module ever.

Should we move all the telescopes outside of contrib and into a library or into base?

I don't think we should: right telescopes indexed by a fixed size are a strict subset of right telescopes. So the library is not as general as could be.

I just realised it's not clear to me what's the objection:

• to move it outside contrib? (And therefore it should stay in contrib)
• to move it outside contrib and into its own library? (And therefore it should be moved into base)
• to move it outside contrib and into base? (And therefore it should be moved somewhere else)

I'm against making it part of base because it's a corner case of a more general theory.